Iof proof for Lemma list extensionality:
1. T : Type
2. T List
3. u : T
4. v : T List
5.
b:(T List). (||v|| = ||b||) 
(i:
. (i < ||v||) (v[i] = b[i])) (v = b)
6. T List
7. u1 : T
8. v1 : T List
9. (||[u / v]|| = ||v1||)
(i:. (i < ||[u / v]||) ([u / v][i] = v1[i])) ([u / v] = v1)
10. ||v||+1 = ||v1||+1
11.
i:. (i < (||v||+1)) ([u / v][i] = [u1 / v1][i])
[u / v] = [u1 / v1]
by ((EqCD)
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 1000:n
C)) (first_tok :t) inil_term)))
C1: .....subterm..... T:t1:n
C1: u = u1
C2: .....subterm..... T:t2:n
C2: v = v1
C.